T, T':Type{i}, L:T List, f:({x:T| (x  L) }T'), P:(T'T'Prop{i'}).
(x, y:T. (x  L)  (y  L)  P(f(x),f(y)))  (x,ymapl(f;L).P(x,y)) 

latex

Definitions	x:A. B(x), Prop, P  Q, x(s1,s2), mapl(f;l), map(f;as), Y, True, Top, x,y. t(x;y), t  T, P & Q, P  Q, {T}, l[i], {i..j}, ||as||, i  j < k, hd(l), nth_tl(n;as), if b t else f fi, ij, b, i<j, true, false, xL. P(x), x:A. B(x), A & B, P  Q, P  Q, (x  l)
Lemmas	pairwise-nil, l member wf, pairwise-cons, cons member, select member, length wf1, non neg length, mapl wf, le wf